equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
A trigonometric identity is (formally) a commutative diagram in the category of cartesian spaces and partial functions whose edges are labelled by rational functions (or sometimes algebraic functions) and trigonometric functions.
Slightly more precisely: each rational function is interpreted as a partial function where is the “natural domain” of (see rational function for more discussion); these are partial analytic functions. The basic trigonometric functions sine () and cosine () are (total) analytic functions . All of these may be interpreted as partial functions , and generate a class of functions by applying the monoidal category structure on the category of partial functions that is induced by the cartesian product on cartesian spaces. A trigonometric identity is then (formally) an equality of morphisms in the monoidal category thus generated.
Of course, this is complete overkill; category theorists are not oblivious to the fact that this is exactly the kind of description lampooned in Linderholm’s Mathematics Made Difficult. It’s just a formal way of covering bases. So let us add that in practice, a trigonometric identity usually involves functions obtained by substituting trigonometric functions into rational functions, or substituting rational linear (affine) functions into trigonometric functions: the class of functions considered is usually fairly limited in scope.
Virtually all trigonometric identities can be seen as arising from suitable exponential function identities on complex numbers such as
,
.
These imply relations between the sine function and the cosine function as follows:
which in turn implies
etc.
See also trigonometric function for some discussion.
See also
Last revised on May 10, 2019 at 15:10:41. See the history of this page for a list of all contributions to it.